T, T':Type, L:(T List), y:T', f:({x:T| (x  L)} T').
(y  mapl(f;L))  (a:T. ((a  L) c (y = f(a)))) 

latex

Definitions	t  T, , {T}, P  Q, ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), i  j < k, Y, ||as||, {i..j}, l[i], P & Q, A c B, x:A. B(x), (x  l), P  Q, P  Q, x:A. B(x), P  Q
Lemmas	mapl wf, cons member, l member wf, non neg length, length wf1, select member